$\forall$$D$:Dsys, ${\it dec}$:($j$,$b$:Id$\rightarrow$M($j$).state$\rightarrow$(M($j$).da(locl($b$))+Unit)). d{-}chooser($D$;${\it dec}$) $\in$ Prop